p:(IdLnk List). lpath(p)   

latex

Definitions	x:A. B(x), t  T, , lpath(p), P & Q, A, P  Q, A  B, False, {i..j}, i  j < k
Lemmas	int seg wf, length wf1, IdLnk wf, Id wf, ldst wf, select wf, lsrc wf, not wf, lnk-inv wf